T:Type, x1,x2:T, L1,L2:(T List).
sublist(T; cons(x1; L1); cons(x2; L2))
 (((x1 = x2)  sublist(T; L1; L2))  sublist(T; cons(x1; L1); L2)) 

latex

Definitions	prop{i:l}, t  T, Y, ||as||, P  Q, P  Q, P  Q, P  Q, sublist(T; L1; L2), P  Q, x:A. B(x), suptype(S; T), subtype(S; T), x:A. B(x), guard(T), sq_type(T), False, A, A  B, increasing(f; k), lelt(i; j; k), int_seg(i; j), True, T, , ff, tt, if b then t else f fi , decidable(P), nequal(T; a; b), Unit, ,
Lemmas	sublist wf, non neg length, neg assert of eq int, assert of eq int, length wf1, int seg wf, eq int wf, decidable assert, length cons, select wf, increasing wf, select cons hd, increasing lower bound, le wf, select cons tl, squash wf, not functionality wrt iff, assert of bnot, eqff to assert, eqtt to assert, iff transitivity, not wf, bnot wf, assert wf, bool wf, true wf